We present here a slightly different formalization of the $\evol{}$ calculus \cite{BGPZFMOODS,BGPZ} that features restriction, abstractions and concretions.

The $\evol{}$ calculus %in the sequel) 
is a variant of CCS \cite{Milner89} without relabeling, 
and extended with constructs for evolvability. 
As in CCS, in $\evol{}$, 
processes can perform actions or synchronize on them.  
We presuppose a countable
set $\ioname$ of names, ranged over by $a,b$, possibly decorated as 
$\overline{a},  \overline{b} \ldots $. As customary, we use $a$ and $\outC{a}$ to denote atomic input and output actions, respectively.
We also assume a countable set $\luname$ of higher order names ranged over by $k,l \dots$ possibly decorated as $k_x, l_x \ldots$ that are used to denote locations and update actions respectively. Finally let $\mathcal{X}$ be a countable set of process variables ranged over by $X, Y, \dots$ and $\mathcal{N} = \ioname \cup \luname$.
The syntax of $\evol{}$ processes 
extends that of CCS with 
 primitive notions of \emph{adaptable processes} $\component{l}{P}$
 and \emph{update prefixes} $\update{l}{U(x)}$:

\todo{riflettere se mettere ricorsione invece di bang e se mettere o meno la somma
ho tolto i pallini e messo le variabili, ho tolto anche la tilde sull'update che faceva confusione}


\todo{secondo me si puo' togliere la continuazione da update: infatti potrei simularla cosi':
$$ \update{l}{P_1}.P_2 ::= \restr{a} \update{l}{a.P_1} \parallel \outC{a}.P_2  $$
}

\begin{definition}[\evol{}]\label{d:finiteccs}
The class of $\evol{}$ \emph{processes}  is described by the following
grammar: 
$$
\begin{array}{lcl}
P    &   ::= &\component{l}{P} \sepr \update{l}{U(x)}.P \sepr P \parallel P  \sepr ! P \sepr P + P  \sepr \restr{a}{P} \sepr a.P \sepr \outC{a}.P  \\
U        &::=& \component{l}{U} \sepr U \parallel U  \sepr ! U \sepr U + U  \sepr \restr{n}{U}  \sepr a.U \sepr \outC{a}.U \sepr \update{l}{U(x)} \sepr x\\
F & ::= & (X)U \todo{check here, not sure about the best way of defining this}\\
C & ::= & \restr{a}{C} \sepr \conc{P}{\nil} \sepr \conc{U}{P} \todo{ dovrebbe essere sempre solo $\conc{C}{}$,  potrebbe essere $ \conc{U}{U}$ credo di no ma controllare}
\end{array}
$$
where   $n \in \ioname$, $U$ are the \emph{update patterns}, $F$ the abstraction and $C$ the concretions.
\end{definition}
\todo{descrizione tutta da sistemare, commentata per ora}

Intuitively, update patterns above represent
a context. The intention is that when an update prefix is able to interact, the current state of  an adaptable process named $l$ is used to replace the variable $x$ in the update pattern $U(x)$. 
Given a process $P$, 
process $\component{l}{P}$ denotes 
the adaptable process $P$ \emph{located at} $l$.
Notice that $l$ acts as a \emph{transparent} locality: process $P$ can evolve on its own, and  interact freely with external processes.
Localities can be nested, so as to form suitable hierarchies of adaptable processes.
The rest of the syntax follows standard lines.
A process $\pi.P$ performs prefix $\pi$ and then behaves as $P$. 
Parallel composition $P \parallel Q$ decrees the concurrent execution of $P$ and $Q$.
%We abbreviate $P_{1} \parallel \cdots \parallel P_{n}$ as $\prod_{i=1}^{n} P _{i}$, and
%use $\prod^{k} P$ to denote the parallel composition of $k$ instances of process $P$.
%Given an index set $I = \{1,..,n\}$, the guarded sum $\sum_{i \in I} \pi_{i}.P_{i}$ represents an exclusive choice
%over $\pi_{1}.P_{1}, \ldots, \pi_{n}.P_{n}$.
%As usual, we write $\pi_{1}.P_{1} + \pi_{2}.P_{2}$ if ${|}I{|}=2$, and $\nil$ if $I$ is empty. 
Process $!\, \pi.P$ defines guarded replication, i.e.,  infinitely many occurrences of $P$ in parallel, which are triggered by prefix $\pi$. Process $\restr{a}{P}$ represent the usual restriction operator, hiding name $a$ in $P$. Notice that location name cannot be hided.
 
The process semantics
is given in terms of a 
Labeled Transition System (LTS). It 
is  generated by the set of rules in Figure \ref{fig:ltswithalpha}.
In addition to the standard CCS actions (input, output, $\tau$), we consider two
complementary actions for process update: 
$\update{l_x}{U}$ and $\component{l}{P}$.
The former represents the possibility to enact an update pattern $U$ for the adaptable process at $l$;
the latter 
says that 
an adaptable process at $l$, with current state $P$, 
can  
be updated. 

\begin{definition}\label{d:srtcong}
\emph{Structural congruence} is  the smallest
congruence relation generated by the following laws: 
$$
\begin{array}{l}
P \parallel Q \equiv Q \parallel P \\ 
P \parallel (Q \parallel R) \equiv (P \parallel Q) \parallel R \\
 P + Q \equiv Q +P.
 \todo{to add rules on restriction}
\end{array}
$$
\end{definition}

We define $\arro{~~~}$ as $\equiv \arro{~\tau~} \equiv $, and write $P \arro{~\alpha}$ if $P \arro{~\alpha} P'$, for some $P'$.


\begin{definition}[LTS for $\evol{}$]\label{d:lts}
The LTS for \evol{}, denoted $\arro{~\alpha~}$,  
is defined by the rules in Figure \ref{fig:ltswithalpha}, with transition labels defined as:

\[
\alpha    ::=  ~~ a \sepr \outC{a} \sepr \up{l} \sepr \loc{l} \sepr \tau
\]
\end{definition}

\begin{figure}[t]
$$
\inferrule[\rulename{Upd}]{}{\update{l}{U(x)} \arro{~\up{l}~}  (x)U.P}
\qquad
\inferrule[\rulename{Comp}]{}{\component{l}{P} \arro{~\loc{l}~} \conc{P} }
\qquad 
\inferrule[\rulename{Act}]{}{\pi.P \arro{~\pi~}  P ~~(\pi \in \{a, \outC{a}\})}
\qquad
$$
$$
\inferrule[\rulename{Loc}]{P \arro{~\alpha~} P'}{\component{l}{P} \arro{~\alpha~}  \component{l}{P'}}
\qquad
\inferrule[\rulename{Sum1}]{P_1 \arro{~\alpha~} P_1'}{P_1 + P_2 \arro{~\alpha~} P'_1 }	
\qquad
\inferrule[\rulename{Repl}]{P \arro{~\alpha~} P'}{!P \arro{~\alpha~} P' \parallel !P }
\qquad
\inferrule[\rulename{Restr}]{P \arro{~\alpha~} P' }{\restr{n}{P} \arro{~\alpha~} \restr{n}{P'}}
$$
$$	
\inferrule[\rulename{Act1}]{P_1 \arro{~\alpha~} P_1'}{P_1 \parallel P_2 \arro{~\alpha~} P'_1 \parallel P_2}	
\qquad
\inferrule[\rulename{Tau1}]{P_1 \arro{~\pi~} P_1' \andalso P_2 \arro{~\outC{\pi}~} P'_2}{P_1 \parallel P_2 \arro{~\tau~}  P'_1 \parallel P'_2}
\qquad
\inferrule[\rulename{Tau3}]{P_1 \arro{~\up{l}~} F \andalso P_2 \arro{~\loc{l}~} C}{P_1 \parallel P_2 \arro{~\tau~}  F \bullet C} 
$$

\caption{LTS for \evol{} .
Rules \rulename{Sum2}, \rulename{Act2}, \rulename{Tau2}, and \rulename{Tau4}---the symmetric counterparts of \rulename{Sum1}
\rulename{Act1}, \rulename{Tau1}, and \rulename{Tau3}---have been omitted.} \label{fig:ltswithalpha}
\end{figure}
 

%
%In Figure \ref{fig:ltswithalpha}, rule \rulename{Upd} represents the contribution of a process at $a$ in an update operation; 
%we use  $\star$ to denote a unique placeholder.
%Rule \rulename{Loc}
%formalizes
%transparency of localities.
%Rules \rulename{Sum}, \rulename{Repl}, 
%\rulename{Act1},
%and \rulename{Tau1} 
% are standard.
% Rule \rulename{Tau3} formalizes process evolvability.
%To realize the 
%evolution of an adaptable process at $l$, it requires: 
%(i)  a process $Q$---which represents its current state; 
%(ii) an update action offering an update pattern  $U$ for updating the process at $l$---which is represented in $P'_{1}$ by $\star$ (cf. rule \rulename{Comp})
%As a result,  
%$\star$ in $P'_{1}$ is replaced with process $\fillcon{U}{Q}$. Notice that this means that  
%the locality 
%being updated is discarded unless it is re-created by $\fillcon{U}{Q}$. 

The application of an abstraction to a concretion is a commutative operation $F \bullet C = C \bullet F$ such that if  $F = D[(x)U.P]$ and $C=E[\conc{R}]$ then 
$$F \bullet C := D[P] \parallel E[U\sub{R}{x}]$$
where $D$ and $E$ are contexts



We introduce some definitions that will be useful in the following.
We denote with $\rightarrow^*$ the
reflexive and transitive
closure of the relation $\rightarrow$.
